type witness
とある値？
多相的な値に対する型情報を使って、型検査時にそれを利用できる
In simple terms, a runtime witness is a value that in some way holds some type-level information associated with a polymorphic value and makes it available to the type checking process.
先にGADTsをちゃんと理解したいmrsekut.icon GADTを使った幽霊型のような感じがあるmrsekut.icon
仕様を満たした型の作り方のいち案として、↓こういうのもあるよ、というのを提案している code:hs
data User (ut :: UserPrivilege) = User { userId :: Integer, userName :: String }
これ、値のfieldにadminとかを持たせずに、型でのみやるということだけど、
わざわざこれを選択する理由はなにか？
値で持っているか否かは、ここではあまり重要ではない
重要なのは、型レベルで「そのUserはAdminである」ことを判別できるかどうか
↓このような定義だとそれができない
code:hs
data User = User { userId :: Integer, userName :: String, userPrivilege :: UserPrivilege }
if userPrivilege == Adminみたいなことを書けば分岐はできるけど、型レベルでそれができていない
このままだとアドミンのみを受け取る関数を型安全に定義できない
GADT復習してもっかい読もう
てをうごかして確認したほうがいい